Wednesday Code and Notes (Week 2)

//proctype: process type
//a process that we could spawn instances of
//if we felt like it
proctype P(byte id) {
  /*_pid: short for process ID
          that is a number assigned to each running process
   */
  printf("================ Hello world, my PID is %d and my ID is %d!\n",_pid,id);
  /*
   pid is unique among *running* processes,
   but not unique over all time.
   You can have two distinct procs with the same PID,
    if their lifetimes don't overlap.
   Global max: 255 processes at a time
   */
}

/*
  init: a special process that will be active
        at startup.
 */
init {
  run P(1);
  run P(2);
  run P(3);
}

//proctype: process type
//a process that we could spawn instances of
//if we felt like it
proctype P(byte id) {
  /*_pid: short for process ID
          that is a number assigned to each running process
   */
  printf("================ Hello world, my PID is %d and my ID is %d!\n",_pid,id);
  /*
   pid is unique among *running* processes,
   but not unique over all time.
   You can have two distinct procs with the same PID,
    if their lifetimes don't overlap.
   Global max: 255 processes at a time
   */
}

/*
  init: a special process that will be active
        at startup.
 */
init {
  /* For systems with fixed number of processes,
     it's good manners to spawn them all at the same
     time, instead of as separate events.

     To do so, we can use
       "atomic"
   */
  atomic {
    run P(1);
    run P(2);
    run P(3);
  }
}

// shared counter variable
byte c = 0;

proctype counter() {
  // these variables are local to (an instance of) counter
  byte temp = 0;
  byte i = 0;
  /* when we execute a do statement:
     - non-deterministically choose a
       non-blocking branch (delimited by ::)
       the first statements of each branch
       is a conditional.
       conditionals block if they are false.
     - if every branch is blocking,
       we're deadlocked!
   */
  do
  :: i < 10 ->
     temp = c;
     c = temp + 1; // this and the previous line are separate
                   // so that we follow the LCR restriction
     i = i + 1;
  :: i >= 10 ->  // why on earth this?
       // we could say else instead of i >= 10
     break;
  od
}

init {
  run counter();
  run counter();
  _nr_pr == 1; // guard: blocks until the conditional becomes true
               // _nr_pr counts the number of running procs
  assert(2 <= c && c <= 20);
}

bit turn = 0

proctype P() {
  // non-critical section
  do
  :: do
     :: true -> break
     :: true -> skip
  od;
  // pre-protocol
waitp: turn == 0;
  // critical section
csp: skip
  // post-protocol
  turn = 1
  od
}

proctype Q() {
  do
  :: do
     :: true -> break
     :: true -> skip
     od;
waitq: turn == 1;
csq: skip
  turn = 0
  od
}

init {
      run P();
      run Q();
}

ltl mutex {[]!(P@csp && Q@csq)}
ltl eeP {[](P@waitp implies <>P@csp)}
ltl eeQ {[](Q@waitq implies <>Q@csq)}